Title: Haskell Magic: Making hylos faster
Date: 2017-09-10
Modified: 2017-12-07
Category: Blog
Slug: haskell-magic-making-hylos-faster
Tags: haskell-magic, haskell
Summary: How to make hylomorphisms run faster

This is a follow-up to my [previous post on this subject][1], which talked about
hylomorphisms from a purely semantic (and usage-oriented) point of view.
However, since then, someone brought [Bananas in Space][2] to my attention. This
rather neat paper, in addition to many other things, discusses a few
optimizations which we can safely make to a range of recursion schemes, due to
the formal guarantees that they provide. The one for hylomorphisms is neat
and elegant, but is given scant mention by the authors, due to it being so
obvious (at least to them). Given that we're not all as smart as they are, I
figured a blog post elucidating this particular optimization would be cool. In
addition, the correctness proof for their improved hylomorphism is such a great
example of [equational reasoning][3] (at least, in my opinion) that I wanted to
share it with the world. 

Without further ado, let's begin.

## Recap ##

For clarity, here are a bunch of definitions that we'll
need throughout this post. All of these are described in more detail in [my
previous post][1], as well as the links therein.

    :::haskell
    import Control.Category ((>>>))

    type Algebra f a = f a -> a
    type Coalgebra f a = a -> f a

    newtype Term f = In { out :: f (Term f) }
    
    cata :: Functor f => Algebra f a -> Term f -> a
    cata f = out >>> fmap (cata f) >>> f

    ana :: Functor f => Coalgebra f a -> a -> Term f
    ana f = f >>> fmap (ana f) >>> In

    hylo :: Functor f => Coalgebra f a -> Algebra f b -> a -> b
    hylo f g = ana f >>> cata g

Now, this definition of a hylomorphism is certainly *correct*, but at the same
time, it's not as efficient as it could be. The reason for this? We have to
complete ``ana f`` before we can get started on ``cata g``, which means we'll
need to build up the *entire* intermediate structure before tearing it down,
even if we don't need to. While in some cases, our compiler might be able to
optimize this away, it's not necessarily a given, especially if what we're doing
is complex.

## Doing it better ##

Luckily for us, [Meijer and Hutton][2] wrote an improved definition of hylomorphisms:

    :::haskell
    hylo' :: Functor f => Coalgebra f a -> Algebra f b -> a - > b
    hylo' f g = f >>> map (hylo' f g) >>> g

There are a few nice things about it:

1. *Provably* equivalent in terms of semantics to the previous definition
1. Doesn't rely on the compiler to optimize generation of the intermediate
   structure
1. No longer depends on ``ana`` and ``cata`` at all (and can be used to define
   both if needs be)

We'll now examine, and demonstrate, each of these claims, and why they are true,
in turn.

### Equivalence ###

In order to make sure that ``hylo'`` is correct, we have to demonstrate that *no
matter* what algebra and coalgebra you give it, and what initial value is fed to
it, we will get the same outcome as if we had used ``hylo`` instead. Something
like this requires a proof - and in languages other than Haskell, this might be
a hard ask. Luckily for us, thanks to Haskell's strong immutability and purity
guarantees, we can use a technique called [*equational reasoning*][3].
Essentially, if we start with *x*, and then make some finite number of
replacements of forms with other, equivalent forms, to produce *y*, we know that
the semantics of *x* and *y* are the same. So let's try that.

We're going to make use of a few such equivalent forms, so let's first discuss
them. One really obvious equivalence we can exploit is that a function's
definition is always equivalent to a call. For example:

    :::haskell
    square :: Int -> Int
    square x = x * x

    {- 
    Every time we see:

    square n

    We can replace it with:

    n * n

    Likewise, every time we see:

    m * m

    We can replace it with:

    square m
    -}

As obvious as this might seem, not every language can make such promises, mostly
because of side effects. Thanks to Haskell keeping these isolated, and forcing
us to be honest if a function ever performs them, we can reason this way in
general. Another obvious equivalence is the duality of a newtype constructor and
its 'unwrapper' function:

    :::haskell
    newtype Foo x = { unFoo :: x }

    {-
    Every time we see:

    Foo >>> unFoo

    We can replace it with:

    id
    -}

Yet another useful equivalence for us is the *associativity* of ``(>>>)``;
whenever we have ``f >>> g >>> h``, it doesn't matter if we do ``(f >>> g) >>>
h`` or ``f >>> (g >>> h)``, as the result will be the same. This is actually a
requirement of the [laws of ``Category``][4]. The only (reasonably) non-obvious
equivalence we will use is the second functor law:

    :::haskell
    forall f g . fmap f >>> fmap g == fmap (f >>> g)

This law is actually a [free theorem][5] in Haskell, and [follows directly][6] from
the first functor law (``fmap id == id``). Surprisingly enough, this is
*everything* we will need to demonstrate the equivalence of ``hylo`` and
``hylo'``!

So, let's begin. Let ``f`` be a coalgebra and ``g`` be an algebra. We start
with:

    :::haskell
    hylo f g

By replacing ``hylo`` with its definition, we get:

    :::haskell
    ana f >>> cata g

By replacing both ``ana`` and ``cata`` with their respective definitions, we
get:

    :::haskell
    (f >>> fmap (ana f) >>> In) >>> (out >>> fmap (cata g) >>> g)

Thanks to the associativity of ``(>>>)``, we can re-bracket this:

    :::haskell
    (f >>> fmap (ana f)) >>> (In >>> out) >>> (fmap (cata g) >>> g)

Seeing as ``In`` is a newtype constructor and ``out`` is its 'unwrapper', we can
replace ``(In >>> out)`` with ``id``. As ``id`` simply returns its argument
as-is, we can remove it from the 'pipeline' above:

    :::haskell
    (f >>> fmap (ana f)) >>> (fmap (cata g) >>> g)

Again, some re-bracketing enabled by the associativity of ``(>>>)``:

    :::haskell
    f >>> (fmap (ana f) >>> fmap (cata g)) >>> g

Now, by applying the second functor law, we get:

    :::haskell
    f >>> fmap (ana f >>> cata g) >>> g

However, as we know, ``ana f >>> cata g`` is just ``hylo f g``:

    ::haskell
    f >>> fmap (hylo f g) >>> g

This is just the definition of ``hylo'`` with a different name. Thus, our proof
by equational reasoning is complete.

### Improved efficiency ###

Let's now see what effect this can have on an existing problem: my mergesort
example from last time. Here's its code, for clarity:

    :::haskell
    import qualified Data.Vector as V
    import Control.Monad.Trans.State

    merge :: Ord a => V.Vector a -> V.Vector a -> V.Vector a
    merge v1 v2 = evalState (V.replicateM totalLength go) (0,0)
        where v1Length = V.length v1
              v2Length = V.length v2
              totalLength = v1Length + v2Length
              go = do (f1, f2) <- get
                      if f1 < v1Length && (not (f2 < v2Length) || (v1 V.! f1 <= v2 V.! f2))
                      then put (f1 + 1, f2) >> return (v1 V.! f1)
                      else put (f1, f2 + 1) >> return (v2 V.! f2)

    data WorkTreeF a s = Leaf a | Bin s s

    instance Functor (WorkTreeF a) where
        fmap _ (Leaf x) = Leaf x
        fmap f (Bin x y) = Bin (f x) (f y)

    breakDown :: Coalgebra (WorkTreeF (V.Vector a)) (V.Vector a)
    breakDown v = case V.length v of
        1 -> Leaf v
        x -> let half = x `div` 2 in
          Bin (V.slice 0 half v) (V.slice half (x - half) v)

    mergeAlg :: Ord a => Algebrea (WorkTreeF (V.Vector a)) (V.Vector a)
    mergeAlg (Leaf v) = v
    mergeAlg (Bin v1 v2) = merge v1 v2

    mergeSort :: Ord a => V.Vector a -> V.Vector a
    mergeSort = hylo breakDown mergeAlg

So let's see what happens when we use ``hylo'`` to mergesort the array ``[2, 3,
1, 1, 10, 0, 14, 4]``. According to ``hylo'``, we have to first feed our array
to our coalgebra. As our array has more than 1 element, that means we construct
a two-leaf ``WorkTreeF`` that looks like this:

<img alt="A tree with two nodes: [2,3,1,1] and [10,0,14,4]" 
  src="{static}/images/hylosort-1.svg">

Next, we have to ``fmap hylo'`` over this structure using the same algebra and
coalgebra we started with. By our definition, we first have to apply ``hylo'``
to the left subtree. Finding a ``Leaf`` storing a non-empty array there, we
repeat the process, applying the coalgebra to make another two-leaf tree:

<img alt="The same tree with the [2,3,1,1] node split into a subtree containing
[2,3] and [1,1]" src="{static}/images/hylosort-2.svg">

After *that*, we have to ``fmap hylo'`` again, and as previously, we must first
do it to the left subtree. Eventually, we'll end up here, having created two
``Leaf`` nodes containing singleton arrays:

<img alt="The tree with the newly split [2,3] node split into a subtree
containing [2] and [3]" src="{static}/images/hylosort-3.svg">

However, at this point, ``fmap hylo'`` will do nothing - there's no more
dividing we can do. Thus, by definition, we now have to apply our catamorphism,
giving us back our singleton arrays on each side:

<img alt="An identical tree after having the catamorphism applied to [2] and
[3]" src="{static}/images/hylosort-4.svg">

We then have to apply our catamorphism again to merge them:

<img alt="The tree after applying the catamorphism to the subtree containing [2]
and [3]. The subtree has been replaced by a single node [2,3]." 
  src="{static}/images/hylosort-5.svg">

Repeating this process, we eventually collect together the entire left subtree
of the root:

<img alt="A tree with two nodes: [1,1,2,3] and [10,0,14,4]" 
  src="{static}/images/hylosort-6.svg">

There are two important observations we can make:

* Throughout this entire time, the right subtree of the root has not been
  touched
* Now that we're about to 'start' on the right subtree, the left subtree has
  been fully collapsed

Thus, we never actually have to generate the entire structure - we only have to
have one branch fully 'materialized' at any one time. While in theory, a good
compiler could do this for us without forcing us to rewrite ``hylo``, doing it
ourselves gives us two good outcomes:

* We can be *sure* that it happens; and
* It will now benefit *everything* we wrote using hylos, regardless of what they
  operate on.

### Recovering the ana- and catamorphism ###

Having gotten rid of ``ana`` and ``cata`` for defining hylomorphisms, we'll now
demonstrate that, in fact, we can define both of them using ``hylo'``:

    :::haskell
    ana' :: Functor f => Coalgebra f a -> a -> Term f
    ana' f = hylo' f In

    cata' :: Functor f => Algebra f a -> Term f -> a
    cata' = hylo' out

These definitions become more obvious when we consider the types of ``In`` and
``out``:

    :::haskell
    In :: f (Term f) -> Term f
    -- that is, Algebra f (Term f)
    out :: Term f -> f (Term f)
    -- that is, Coalgebra f (Term f)

We can also do some equational reasoning to reconstruct our original definition
for ``ana`` and ``cata``. For ``ana``, the chain of substitutions goes like
this:

    :::haskell
    ana' f -- initial
    hylo' f In -- by definition of ana'
    f >>> fmap (hylo' f In) >>> In -- by definition of hylo'
    f >>> fmap (ana' f) >>> In -- by definition of ana'

While for ``cata``, it goes like this:

    :::haskell
    cata' f-- initial
    hylo' out f -- by definition of cata'
    out >>> fmap (hylo' out f) >>> f -- by definition of hylo'
    out >>> fmap (cata' f) >>> f -- by definition of cata'

Clearly, aside from a slight difference in naming, we've recovered both ``ana``
and ``cata`` only using ``hylo'``.

## Conclusion ##

We've taken a fun tour of how we can improve ``hylo``, and discovered
some clever things along the way. Additionally, I hope that this can demonstrate
the benefits of Haskell, if not least of all due to the power of equational
reasoning. Remember, think hard and have fun!

[1]: https://retro-freedom.nz/haskell-magic-hylomorphisms-and-divide-and-conquer.html
[2]: https://pdfs.semanticscholar.org/b7ce/0fa52dfaaf8c4999e73797e0a20cc2576d12.pdf
[3]: http://www.haskellforall.com/2013/12/equational-reasoning.html
[4]: http://hackage.haskell.org/package/base-4.10.0.0/docs/Control-Category.html#t:Category
[5]: https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
[6]: https://github.com/quchen/articles/blob/master/second_functor_law.md
